Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    from(X)  → cons(X,n__from(s(X)))
2:    head(cons(X,XS))  → X
3:    2nd(cons(X,XS))  → head(activate(XS))
4:    take(0,XS)  → nil
5:    take(s(N),cons(X,XS))  → cons(X,n__take(N,activate(XS)))
6:    sel(0,cons(X,XS))  → X
7:    sel(s(N),cons(X,XS))  → sel(N,activate(XS))
8:    from(X)  → n__from(X)
9:    take(X1,X2)  → n__take(X1,X2)
10:    activate(n__from(X))  → from(X)
11:    activate(n__take(X1,X2))  → take(X1,X2)
12:    activate(X)  → X
There are 7 dependency pairs:
13:    2nd#(cons(X,XS))  → HEAD(activate(XS))
14:    2nd#(cons(X,XS))  → ACTIVATE(XS)
15:    TAKE(s(N),cons(X,XS))  → ACTIVATE(XS)
16:    SEL(s(N),cons(X,XS))  → SEL(N,activate(XS))
17:    SEL(s(N),cons(X,XS))  → ACTIVATE(XS)
18:    ACTIVATE(n__from(X))  → FROM(X)
19:    ACTIVATE(n__take(X1,X2))  → TAKE(X1,X2)
The approximated dependency graph contains 2 SCCs: {15,19} and {16}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.50 seconds)   ---  May 3, 2006